\begin{tabbing}
ecl{-}trans{-}act(${\it ds}$;${\it da}$;$A$)($n$,$L$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\exists$${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List, ${\it tr}$:event{-}info(${\it ds}$;${\it da}$).\+
\\[0ex]$L$ $=$ (${\it L'}$ @ [${\it tr}$])
\\[0ex]\& \=let $k$,$s$,$v$ = ${\it tr}$ in \+
\\[0ex]($k$ $\in$ ecl{-}trans{-}ks($A$)) \& ecl{-}trans{-}a($A$)($n$,$k$,$s$,$v$,ecl{-}trans{-}state($A$;${\it L'}$))
\-\-
\end{tabbing}